\subsection{Scheduling}\label{subsec:scheduling}
After system initialization is complete, the kernels running on the different
logical processors synchronize and start scheduling subjects. Which subject to
schedule on what particular CPU is defined by the scheduling plan. A policy
writer defines the system's scheduling regime in the XML policy file, see
listing \ref{lst:xml-scheduling-plan} for an example.

The example scheduling plan of listing \ref{lst:xml-scheduling-plan} contains
four subjects which are scheduled on two logical processors. The Muen policy
compiler transforms the scheduling plan in XML format to SPARK specifications
which are directly compiled into the kernel. The scheduling plan is therefore
static at compilation time and cannot be modified at runtime.

\begin{lstlisting}[
	language=xml,
	label=lst:xml-scheduling-plan,
	caption=System scheduling plan in XML]
<scheduling tick_rate="10000">
	<major_frame>
		<cpu>
			<minor_frame subject_id="1" ticks="40"/>
			<minor_frame subject_id="2" ticks="40"/>
		</cpu>
		<cpu>
			<minor_frame subject_id="3" ticks="80"/>
		</cpu>
	</major_frame>
	<major_frame>
		<cpu>
			<minor_frame subject_id="1" ticks="80"/>
		</cpu>
		<cpu>
			<minor_frame subject_id="4" ticks="80"/>
		</cpu>
	</major_frame>
</scheduling>
\end{lstlisting}

Each kernel stores the index of the active minor frame in its per-CPU storage
area. The index points into the current scheduling major frame. Initially, this
value is set to one\footnote{\texttt{Minor\_Frame\_Range'First}}, i.e. the
first minor frame in the active major frame.

The index designating the current major frame is global and therefore identical
for all kernels. This index is managed by the privileged $\tau$0 subject and
only read by the kernels.

The minor/major frame tuple forms an index into the scheduling plan. It points
to a minor frame containing the subject ID and timer ticks for the next subject
to schedule. The subject ID is used to load the state of the corresponding
subject from the state descriptor array into the processor.

The mechanism used to keep track of time is the VMX preemption timer. Writing
the timer ticks into the subject's VMCS region sets the timer. The kernel then
calls the \texttt{VMLAUNCH} or \texttt{VMRESUME} (if the subject has already
been launched) VT-x instructions to enter VMX non-root operation, which lets the
processor execute subject code.  The subject is then automatically preempted by
the processor when the allotted time slice is over. Figure
\ref{fig:kernel-scheduler} illustrates this process.

\begin{figure}[h]
	\centering
	\input{graph_scheduler}
	\caption{Kernel scheduler}
	\label{fig:kernel-scheduler}
\end{figure}

The subject state is saved on each VM exit. Depending on the scheduling plan and
the exit reason, the state of another subject is loaded by the kernel scheduler.
If the exit occurred because the VMX preemption timer fired, the scheduler is
aware that it must advance to the next minor frame in the current major frame.
This is done by incrementing the current minor frame counter. If the minor frame
index reaches the upper end of the allowed range
(\texttt{Minor\_Frame\_Range'Last}), it is reset to the first value of the
range.
